Nuprl Lemma : fpf-join-empty-sq
11,40
postcript
pdf
A
:Type,
B
:(
A
Type),
f
:
a
:
A
fp
B
(
a
),
eq
:EqDecider(
A
).
f
~ <
f
.1,
a
.(
f
.2)(
a
)>
latex
Definitions
EqDecider(
T
)
,
x
.
t
(
x
)
,
x
(
s
)
,
f
(
a
)
,
Type
,
a
:
A
fp
B
(
a
)
,
x
:
A
B
(
x
)
,
,
f
g
,
f
(
x
)?
z
,
x
dom(
f
)
,
f
(
x
)
,
S
T
,
x
:
A
.
B
(
x
)
,
x
:
A
B
(
x
)
,
type
List
,
Top
,
x
:
A
.
B
(
x
)
,
t
T
,
Void
Lemmas
top
wf
,
filter
tt
,
fpf
wf
,
deq
wf
origin
A:Type, B:(A
Type), f:a:A fp B(a), eq:EqDecider(A). 
f ~ <f.1, 
a.(f.2)(a)> A:Type, B:(AType), f:a:A fp B(a), eq:EqDecider(A). f ~ <f.1, a.(f.2)(a)> 
x. t(x) B(a)
B(x) g
dom(f)
Tx:A. B(x)B(x)
x:A.B(x) T